\begin{tabbing}
ecl{-}add{-}throw($A$;$m$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ea}$ = $A$ in \+
\\[0ex]$\langle$${\it Ta}$
\\[0ex]$,\,$${\it ksa}$
\\[0ex]$,\,$${\it ia}$
\\[0ex]$,\,$${\it ga}$
\\[0ex]$,\,$($\lambda$$n$,$x$. if $n$=$_{2}$$m$$\rightarrow$ ${\it ha}$(0,$x$) $\vee_{2}$ ${\it ha}$($n$,$x$) else 0$<_{2}$$n$ $\wedge_{2}$ ${\it ha}$($n$,$x$) fi)
\\[0ex]$,\,$${\it aa}$
\\[0ex]$,\,$if $m$=$_{2}$0$\rightarrow$ ${\it ea}$ else s{-}insert($m$;${\it ea}$) fi$\rangle$
\-
\end{tabbing}